\begin{tabbing}
es{-}first{-}at{-}since'(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}loc(${\it es}$; $e$) $=$ $i$ $\in$ Id\+
\\[0ex]\& $R$($e$)
\\[0ex]\& (\=$\exists$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}locl(${\it es}$; ${\it e'}$; $e$)
\\[0ex]\& $P$(${\it e'}$) \& ($\forall$${\it e''}$:es{-}E(${\it es}$). es{-}le(${\it es}$;${\it e'}$;${\it e''}$) $\Rightarrow$ es{-}locl(${\it es}$; ${\it e''}$; $e$) $\Rightarrow$ $\neg$$R$(${\it e''}$)))
\-\-
\end{tabbing}